Deduction versus Computation: The Case of Induction
Identifieur interne : 008815 ( Main/Exploration ); précédent : 008814; suivant : 008816Deduction versus Computation: The Case of Induction
Auteurs : Eric Deplagne [France] ; Claude Kirchner [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
English descriptors
Abstract
Abstract: The fundamental difference and the essential complementarity between computation and deduction are central in computer algebra, automated deduction, proof assistants and in frameworks making them cooperating. In this work we show that the fundamental proof method of induction can be understood and implemented as either computation or deduction. Inductive proofs can be built either explicitly by making use of an induction principle or implicitly by using the so-called induction by rewriting and inductionless induction methods. When mechanizing proof construction, explicit induction is used in proof assistants and implicit induction is used in rewrite based automated theorem provers. The two approaches are clearly complementary but up to now there was no framework able to encompass and to understand uniformly the two methods. In this work, we propose such an approach based on the general notion of deduction modulo. We extend slightly the original version of the deduction modulo framework and we provide modularity properties for it. We show how this applies to a uniform understanding of the so called induction by rewriting method and how this relates directly to the general use of an induction principle.
Url:
DOI: 10.1007/3-540-45470-5_3
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003317
- to stream Istex, to step Curation: 003275
- to stream Istex, to step Checkpoint: 001C51
- to stream Main, to step Merge: 008C71
- to stream PascalFrancis, to step Corpus: 000778
- to stream PascalFrancis, to step Curation: 000265
- to stream PascalFrancis, to step Checkpoint: 000813
- to stream Main, to step Merge: 008D98
- to stream Main, to step Curation: 008815
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Deduction versus Computation: The Case of Induction</title><author><name sortKey="Deplagne, Eric" sort="Deplagne, Eric" uniqKey="Deplagne E" first="Eric" last="Deplagne">Eric Deplagne</name></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:D67159921753385256A4754FC54855017C7FAA51</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45470-5_3</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-F0MP86RJ-J/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003317</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003317</idno><idno type="wicri:Area/Istex/Curation">003275</idno><idno type="wicri:Area/Istex/Checkpoint">001C51</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001C51</idno><idno type="wicri:doubleKey">0302-9743:2002:Deplagne E:deduction:versus:computation</idno><idno type="wicri:Area/Main/Merge">008C71</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:03-0367824</idno><idno type="wicri:Area/PascalFrancis/Corpus">000778</idno><idno type="wicri:Area/PascalFrancis/Curation">000265</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000813</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000813</idno><idno type="wicri:doubleKey">0302-9743:2002:Deplagne E:deduction:versus:computation</idno><idno type="wicri:Area/Main/Merge">008D98</idno><idno type="wicri:Area/Main/Curation">008815</idno><idno type="wicri:Area/Main/Exploration">008815</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Deduction versus Computation: The Case of Induction</title><author><name sortKey="Deplagne, Eric" sort="Deplagne, Eric" uniqKey="Deplagne E" first="Eric" last="Deplagne">Eric Deplagne</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA & INRIA, 615 rue du Jardin Botanique, BP 101, 54602, Villers-lès-Nancy Cedex, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA & INRIA, 615 rue du Jardin Botanique, BP 101, 54602, Villers-lès-Nancy Cedex, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Automatic proving</term><term>Computer algebra</term><term>Induction</term><term>Proof theory</term><term>Rewriting</term><term>Theorem proving</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Calcul formel</term><term>Démonstration automatique</term><term>Démonstration théorème</term><term>Induction</term><term>Réécriture</term><term>Théorie preuve</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The fundamental difference and the essential complementarity between computation and deduction are central in computer algebra, automated deduction, proof assistants and in frameworks making them cooperating. In this work we show that the fundamental proof method of induction can be understood and implemented as either computation or deduction. Inductive proofs can be built either explicitly by making use of an induction principle or implicitly by using the so-called induction by rewriting and inductionless induction methods. When mechanizing proof construction, explicit induction is used in proof assistants and implicit induction is used in rewrite based automated theorem provers. The two approaches are clearly complementary but up to now there was no framework able to encompass and to understand uniformly the two methods. In this work, we propose such an approach based on the general notion of deduction modulo. We extend slightly the original version of the deduction modulo framework and we provide modularity properties for it. We show how this applies to a uniform understanding of the so called induction by rewriting method and how this relates directly to the general use of an induction principle.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Deplagne, Eric" sort="Deplagne, Eric" uniqKey="Deplagne E" first="Eric" last="Deplagne">Eric Deplagne</name></region><name sortKey="Deplagne, Eric" sort="Deplagne, Eric" uniqKey="Deplagne E" first="Eric" last="Deplagne">Eric Deplagne</name><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name><name sortKey="Kirchner, Claude" sort="Kirchner, Claude" uniqKey="Kirchner C" first="Claude" last="Kirchner">Claude Kirchner</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008815 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 008815 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:D67159921753385256A4754FC54855017C7FAA51
|texte= Deduction versus Computation: The Case of Induction
}}
| This area was generated with Dilib version V0.6.33. |  |